『定理証明支援系 Coq 入門 SSReflect 中心』
アフェルト レナルド. 定理証明支援系 Coq 入門 SSReflect 中心. 産業技術総合研究所, 2014-09-07
定理証明支援系 Coq 入門 SSReflect 中心
形式化とは
形式検証
ソフトウェア安全性の保証、バグがないことを保証
定理証明支援系の歴史や適用事例など情報多めのスライド
Coqのコード例もとても多い
Heartbleed
CompCert
seL4
マイクロカーネル
定理証明支援系
Coq
HOL Light
Isabelle/HOL
四色定理
Kepler予想
奇数位数定理
Homotopy Type Theory(HoTT)
Univalent Foundations
SSReflect
はCoqのライブラリ
Comon Criteria(CC)
Proof General
CoqIDE
MathComp
ホーア理論
確認用
Q.
参考
関連
#Coq
#定理証明支援系
#文献